package tests.qc.Ix where

import Data.Ix as I
import Test.QuickCheck public


bools = arbitrary:: Gen Bool

chars = arbitrary:: Gen Char

smallInts :: Gen Int

smallInts = choose (0, 10000)

smallIntegers = choose (toInteger 0, toInteger 10000)

leftPairs = do
    a<-choose (0, 100)
    b<-choose (0, 100)
    return (a,b)

rightPairs = do
    a<-choose (90, 200)
    b<-choose (90, 200)
    return (a,b)

allPairs = do
    a<-choose (0, 200)
    b<-choose (0, 200)
    return (a,b)

leftTriples = do
    a<-choose (0, 10)
    b<-choose (0, 10)
    c<-choose (0, 10)
    return (a,b,c)

-- doesn't seem to work 
-- smallTriples = do
--    a<-choose (0, 100)
--    b<-choose (0, 100)
--    c<-choose (0, 100)
--    return (a,b,c)


allTriples = do
    a<-choose (0, 20)
    b<-choose (0, 20)
    c<-choose (0, 20)
    return (a,b,c)

rightTriples = do
    a<-choose (9, 20)
    b<-choose (9, 20)
    c<-choose (9, 20)
    return (a,b,c)

smallPairs = allPairs
smallTriples = allTriples

gte g l = g `suchThat` (>=l)

between g l u = (gte g l) `suchThat` (<=u)

---inRange (l,u) i == elem i (range (l,u))
p_inRange_iff_elem_of_range g1 g2 g3 = forAll g1 (\l ->
        forAll (gte g2 l) (\u ->
            forAll g3 (\i ->
                inRange (l,u) i == elem i (range (l,u))
            )
        )
    )

p_inRange_iff_elem_of_range_bools = p_index_i_gets_i bools
p_inRange_iff_elem_of_range_chars = p_index_i_gets_i chars
p_inRange_iff_elem_of_range_smallInts = p_index_i_gets_i smallInts
p_inRange_iff_elem_of_range_smallIntegers = p_index_i_gets_i smallIntegers
p_inRange_iff_elem_of_range_smallPairs = p_index_i_gets_i smallPairs
-- p_inRange_iff_elem_of_range_smallTriples = p_index_i_gets_i smallTriples


--- @range (l,u) !! index (l,u) i == i@ , when @inRange (l,u) i@
p_index_i_gets_i g1 g2 g3 = forAll g1 (\l ->
        forAll (gte g2 l) (\u ->
            forAll (between g3 l u) (\i ->
                inRange (l,u) i ==> range (l,u) !! index (l,u) i == i
            )
        )
    )

p_index_i_gets_i_bools = p_index_i_gets_i bools
p_index_i_gets_i_chars = p_index_i_gets_i chars
p_index_i_gets_i_smallInts = p_index_i_gets_i smallInts
p_index_i_gets_i_smallIntegers = p_index_i_gets_i smallIntegers
p_index_i_gets_i_smallPairs = p_index_i_gets_i smallPairs
-- p_index_i_gets_i_smallTriples = p_index_i_gets_i smallTriples


--- map (index (l,u)) (range (l,u)) == [0..rangeSize (l,u)-1]
p_index_0_until_rangeSize g1 g2 = forAll g1 (\l ->
         forAll (gte g2 l) (\u ->
                 map (index (l,u)) (range (l,u)) == [0..rangeSize (l,u)-1]
             )
         )

p_index_0_until_rangeSize_bools = p_index_i_gets_i bools
p_index_0_until_rangeSize_chars = p_index_i_gets_i chars
p_index_0_until_rangeSize_smallInts = p_index_i_gets_i smallInts
p_index_0_until_rangeSize_smallIntegers = p_index_i_gets_i smallIntegers
p_index_0_until_rangeSize_smallPairs = p_index_i_gets_i smallPairs
-- p_index_0_until_rangeSize_smallTriples = p_index_i_gets_i smallTriples

--- rangeSize (l,u) == length (range (l,u))
p_rangeSize g1 g2 = forAll g1 (\l ->
         forAll (gte g2 l) (\u ->
                 rangeSize (l,u) == length (range (l,u))
             )
         )

p_rangeSize_bools = p_index_i_gets_i bools
p_rangeSize_chars = p_index_i_gets_i chars
p_rangeSize_smallInts = p_index_i_gets_i smallInts
p_rangeSize_smallIntegers = p_index_i_gets_i smallIntegers
p_rangeSize_smallPairs = p_index_i_gets_i smallPairs
-- p_rangeSize_smallTriples = p_index_i_gets_i smallTriples

